Nuprl Lemma : es-first-at-since_wf 11,40
es:ES, i:Id, e':E, P, R:({e:E| loc(e) = i} ). es-first-at-since(es;i;e';e.R(e);e.P(e))   
latex

Definitionses-first-at-since(es;i;e;e.R(e);e.P(e)), ES, t  T, Id, x:A. B(x), E, , loc(e), x(s), b, P  Q, False, A, P & Q, (e <loc e'), A c B, e loc e' , x:A. B(x), e<e'. P(e), x. t(x)
Lemmasalle-lt wf, es-le wf, es-locl wf, es-le-loc, es-loc-pred, es-loc wf, es-E wf, Id wf, event system wf

origin